(module type-lattice mzscheme
  ;; Provide the lattice operations on types
  (provide weaker-than join meet)
  
  ;; Implements the following lattice over types:
  ;;                                  -- Top ----
  ;;                                /         \   \
  ;;                              Num          \   \
  ;;                               |  \        |   ~>
  ;;                               |   \       |   |
  ;;                             Int   Bool  List  ->   
  ;;                               \     \    /    /
  ;;                                --- Bottom ----
  ;; Note that list 'a is weaker than list 'b iff 'a is weaker than 'b
  ;; Pure arrows are weaker than impure arrows because any pure operation
  ;; can be lifted to a pure operation
  
  (require "types.scm"
           (lib "plt-match.ss")
           (only (lib "1.ss" "srfi") fold))
  
  ;; Special purpose function to handle lists
  (define (list-weaker-than xs ys)
    (fold (lambda (x y ans) (and ans (weaker-than x y))) #t xs ys))
  
  ;; Special purpose function to handle
  (define (arrow-weaker-than arg1 res1 arg2 res2)
    (and (list-weaker-than arg2 arg1)
         (list-weaker-than res1 res2)))
  
  ;; This implements weaker-than or equal-to on the lattice shown above
  (define (weaker-than ty1 ty2)
    (match ty2
      ((struct ty-top ()) (ty-top? ty1))
      ((struct ty-num ())
       (or (ty-num? ty1) (ty-int? ty1) (ty-bool? ty1) (ty-bot? ty1)))
      ((struct ty-bool ()) (or (ty-bool? ty1) (ty-bot? ty1)))
      ((struct ty-int  ()) (or (ty-int? ty1)  (ty-bot? ty1)))
      ((struct ty-list (ty))
       (or (ty-bot? ty1)
           (and (ty-list? ty1)
                (weaker-than ty (ty-list-ty ty1)))))
      ((struct ty-pure-arrow (args2 res2))
       (match ty1
         ((struct ty-pure-arrow (args1 res1))
          (arrow-weaker-than args1 res1 args2 res2))
         (_ (ty-bot? ty1))))
      ((struct ty-impure-arrow (args2 res2))
       (match ty1
         ((struct ty-pure-arrow (args1 res1))
          (arrow-weaker-than args1 res1 args2 res2))
         ((struct ty-impure-arrow (args1 res1))
          (arrow-weaker-than args1 res1 args2 res2))
         (_ (ty-bot? ty1))))
      ((struct ty-bot ())
       (ty-bot? ty1))))
  
  ;; The greatest lower bound of the two types
  (define (join ty1 ty2)
    (if (ty-bot? ty2) ty1
        (match ty1
          ((struct ty-top ()) (type top))
          ((struct ty-num ())
           (match ty2
             ((struct ty-num ())  (type num))
             ((struct ty-int ())  (type num))
             ((struct ty-bool ()) (type num))
             ((struct ty-bot ())  (type num))
             (_ (type top))))
          ((struct ty-int ())
           (match ty2
             ((struct ty-num ())  (type num))
             ((struct ty-int ())  (type int))
             ((struct ty-bool ()) (type num))
             ((struct ty-bot ())  (type int))
             (_ (type top))))
          ((struct ty-bool ())
           (match ty2
             ((struct ty-num ())  (type num))
             ((struct ty-bool ()) (type bool))
             ((struct ty-int ())  (type num))
             ((struct ty-bot ())  (type bool))
             (_ (type top))))
          ((struct ty-list (list-ty1))
           (match ty2
             ((struct ty-list (list-ty2))
              (make-ty-list (join list-ty1 list-ty2)))
             (_ (type top))))
          ((struct ty-pure-arrow (args1 res1))
           (match ty2
             ((struct ty-pure-arrow (args2 res2))
              (make-ty-pure-arrow (map meet args1 args2)
                                  (map join res1 res2)))
             ((struct ty-impure-arrow (args2 res2))
               (make-ty-pure-arrow (map meet args1 args2)
                                   (map join res1 res2)))
             (_ (type top))))
          ((struct ty-impure-arrow (args1 res1))
           (match ty2
             ((struct ty-impure-arrow (args2 res2))
              (make-ty-impure-arrow (map meet args1 args2)
                                    (map join res1 res2)))
             ((struct ty-pure-arrow (args2 res2))
              (make-ty-pure-arrow (map meet args1 args2)
                                  (map join res1 res2)))
             (_ (type top))))
          ((struct ty-bot ()) ty2)
          (_ (type top)))))
           
         
  ;; The least upper bound on the type lattice
  (define (meet ty1 ty2)
    (if (ty-top? ty2) ty1
        (match ty1
          ((struct ty-top ()) ty2)
          ((struct ty-num ())
           (match ty2
             ((struct ty-num ())  (type num))
             ((struct ty-int ())  (type int))
             ((struct ty-bool ()) (type bool))
             (_ (type bot))))
          ((struct ty-int ())
           (match ty2
             ((struct ty-num ()) (type int))
             ((struct ty-int ()) (type int))
             (_ (type bot))))
          ((struct ty-bool ())
           (match ty2
             ((struct ty-num ())  (type bool))
             ((struct ty-bool ()) (type bool))
             (_ (type bot))))
          ((struct ty-list (list-ty1))
           (match ty2
             ((struct ty-list (list-ty2))
              (make-ty-list (meet list-ty1 list-ty2)))
             (_ (type bot))))
          ((struct ty-pure-arrow (args1 res1))
           (match ty2
             ((struct ty-pure-arrow (args2 res2))
              (make-ty-pure-arrow (map join args1 args2)
                                  (map meet res1 res2)))
             ((struct ty-impure-arrow (args2 res2))
              (make-ty-impure-arrow (map join args1 args2)
                                    (map meet res1 res2)))
             (_ (type bot))))
          ((struct ty-impure-arrow (args1 res1))
           (match ty2
             ((struct ty-impure-arrow (args2 res2))
              (make-ty-impure-arrow (map join args1 args2)
                                    (map meet res1 res2)))
             ((struct ty-pure-arrow (args2 res2))
              (make-ty-impure-arrow (map join args1 args2)
                                    (map meet res1 res2)))
             (_ (type bot))))
          ((struct ty-bot ()) (type bot))))))
 